public class Unifier {
    Stack<Variable> bound;
    boolean debug;
    
    public boolean unify(Term x, Term y) {
        return unify(x, y, null);
    }
    
    public boolean unify(Term x, Term y, Stack<Variable> bindings) {
        boolean result;
        
        if(debug) System.out.println(" %% attempting " +x+ " = " +y+ ".");
        
        bound = bindings;
        result = unify_loop(x,y);
        
        if(!result) {
            if(debug) System.out.println(" %% failed...");
            while(bound != null) {
                bound.head.unbind();
                bound = bound.tail;
            }
        }

        if(debug) System.out.println(" %% done...");
        
        return result;
    }
    
    public boolean unify_loop(Term x, Term y) {
        x = x.dereference();
        y = y.dereference();
        if(debug) System.out.println(" %%   sub " +x+ " = " +y+ ".");
        if(x == y) return true;
        if(x.kind == Term.Kind.VARIABLE) {
            Variable xv = (Variable)x;
            if(y.contains(xv)) {
                return false;
            }
            else {
                xv.bindTo(y);
                bound = new Stack<Variable>(xv,bound);
                return true;
            }
        }
        else {
            Compound xc = (Compound)x;
            if(y.kind == Term.Kind.VARIABLE) {
                Variable yv = (Variable)y;
                if(xc.contains(yv)) {
                    return false;
                }
                else {
                    yv.bindTo(xc);
                    bound = new Stack<Variable>(yv,bound);
                    return true;
                }
            }
            else {
                Compound yc = (Compound)y;
                if(debug) System.out.println(" %%   com " +xc.arity+ " & " +yc.arity+ ".");
                if(xc.arity == yc.arity && xc.name.equals(yc.name)) {
                    for(int i = 0; i < xc.arity; i++) {
                        if(!unify_loop(xc.args[i],yc.args[i]))
                            return false;
                    }
                    return true;
                }
                return false;
            }
        }
    }
}

